Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
f
(
f
(
a
,
b
),x)
→
f
(
a
,
f
(
a
,x))
2:
f
(
f
(
b
,
a
),x)
→
f
(
b
,
f
(
b
,x))
3:
f
(x,
f
(y,z))
→
f
(
f
(x,y),z)
There are 6 dependency pairs:
4:
F
(
f
(
a
,
b
),x)
→
F
(
a
,
f
(
a
,x))
5:
F
(
f
(
a
,
b
),x)
→
F
(
a
,x)
6:
F
(
f
(
b
,
a
),x)
→
F
(
b
,
f
(
b
,x))
7:
F
(
f
(
b
,
a
),x)
→
F
(
b
,x)
8:
F
(x,
f
(y,z))
→
F
(
f
(x,y),z)
9:
F
(x,
f
(y,z))
→
F
(x,y)
Consider the SCC {4-9}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.02 seconds) --- May 4, 2006